COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	The McCarthy prize problem
C00008 ENDMK
C⊗;
The McCarthy prize problem

	John McCarthy offers $100 of his own money for the best satisfactory
solution of the following problem.  Solutions must be in writing
and delivered to McCarthy or Nils Nilsson by Friday, July 23, 1982,
and the solvers must be prepared to defend their solutions orally
at SRI on that date.  Unless there is a satisfactory solution, no
prize will be awarded.

	The problem is to give axioms from which the following
piece of chess reasoning can be carried out.  The point isn't
chess, and solutions can use suitable chess lemmas as axioms.
On the other hand, it must be clear that the solution follows
entirely formally from the axioms.  Solutions will be compared,
if there is more than one meeting the formal requirements, according
to how well they express the informal reasoning presented below.


A chess example of reasoning about concurrent actions.

	The chess position of Figure 1 is mentioned in (Berliner 197x).
All he does with it is to remark that unless the lookahead sees very far
ahead, present day programs will keep the white king behind the white
pawns in order to preserve control of the center and hence won't win.
However, the following argument that white can win shows that
chess reasoning involves reasoning about concurrent events even though
the actual moves in chess are sequential.

	We note that black must stay within the eight marked squares or else
white will promote his pawn, and this is assumed to win for white.
White can win by moving his king along the path shown in the
figure and black cannot prevent his reaching b5 without letting
the pawn promote.  When it is white's move with his king on b5, if
the black king is not on c7, then the white king can immediately
advance to c6.  If the black king is on c7, then white moves his king
to a6 and can subsequently move to b6 and then to c6 without further
interference.  When it is white's move with his king on c6, if the
black king is not on e7, then white can capture the black pawn on
d6 - which is assumed to win.  If the black king is on e7, then white
move his king to c7 and can capture the pawn on the next move.

	From the AI point of view, the most interesting part of this argument
is that we do not need to examine in detail what black can do while
white is advancing his king.  All we need to reason about is whether
black stays within the eight squares that prevent the pawn from
queening.  We achieve an enourmous reduction in search space, because
we don't have to do a tree search on the black moves.  However, this
reduction is accomplished by reasoning about concurrent action, namely
"while white is advancing his king, black must stay within the eight
squares and therefore cannot interfere with the advance".  The last
two steps of reasoning, each of which makes a case analysis according to whether
the black king is or is not on a specific square, are also worth noting.

Figure 1 has the white king on d3, the black king on d8, white pawns
on c4, d5, e6, f5 and g4, and black pawns on c5, d6, f6 and g5.

	It seems to me that this problem provides the opportunity for
an advance beyond the simple situation calculus.  The problem is to
give a set of first order axioms that allow a proof that white can
win.  Of course, it is permissible to abstract away the specifically
chess aspects of the problem.